\begin{tabbing}
$\forall$$M_{1}$, $M_{2}$:MsgA.
\\[0ex]$M_{1}$ $\subseteq$ $M_{2}$
\\[0ex]$\Rightarrow$ (\=$\forall$$a$:Id, $s$:$M_{2}$.state.\+
\\[0ex]$a$ declared in $M_{1}$ $\Rightarrow$ unsolvable $M_{2}$.pre($a$,$s$) $\Rightarrow$ unsolvable $M_{1}$.pre($a$,$s$))
\-
\end{tabbing}